LISPAX.PRF[F82,JMC] - www.SailDart.org

perm filename LISPAX.PRF[F82,JMC] blob sn#688564 filedate 1982-11-22 generic text, type T, neo UTF8
(VERS3 0 (NIL ((SIMPINFO (#& . 0) (#& . 9) (#& . 16) (#& . 23) (#& . 28) (#& . 31) (#& . 32) (#& . 33) (#& . 34) (#& . 35) (#& . 36) (#& . 37) (#& . 38) (#& . 39) (#& . 40) (#& . 41) (#& . 42) (#& . 45) (#& . 46) (#& . 49) (#& . 50) (#& . 53) (#& . 54) (#& . 55) (#& . 56) (#& . 64)) (MEMBERDEF (#& . 67)) (ASSOCDEF (#& . 70)) (MKALIST (#& . 71)) (MAPCARDEF (#& . 72)) (SOMEPDEF (#& . 75)) (ALLPDEF (#& . 79)) (APPLASSOC (#& . 81)) (APPRASSOC (#& . 82)) (APPENDEF (#& . 53)) (LISTAPPEND (#& . 50)) (SEXPINDUCTIONDEF (#& . 83)) (SEXPINDUCTION (#& . 92)) (LISTINDUCTIONDEF (#& . 87)) (LISTINDUCTION (#& . 93))) ((CAR #& . 29) (CDR #& . 24) (ATOM #& . 1) (NULL #& . 26) (LISTP #& . 10) (ALISTP #& . 57) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (ZA #& . 5) (YA #& . 7) (XA #& . 8) (C #& . 94) (B #& . 96) (A #& . 97) (PHI #& . 76) (CONS #& . 21) (PARS #& . 84) (FUN #& . 86) (DEF #& . 88) (NILCASE #& . 89) (DEFSEXP #& . 90) (ATOMCASE #& . 91) (LIST #& . 43) (LST #& . 47) (APPEND #& . 51) (ALLP #& . 80) (SOMEP #& . 78) (MAPCAR #& . 73) (FN #& . 74) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63) (ASSOC #& . 65) (MEMBER #& . 68)) (LISPAX (#& . 30) (#& . 25) (#& . 2) (#& . 27) (#& . 11) (#& . 58) (#& . 4) (#& . 13) (#& . 18) (#& . 6) (#& . 95) (#& . 77) (#& . 22) (#& . 0) (#& . 9) (#& . 16) (#& . 23) (#& . 28) (#& . 31) (#& . 32) (#& . 33) (#& . 34) (#& . 35) (#& . 36) (#& . 37) (#& . 38) (#& . 39) (#& . 40) (#& . 41) (#& . 93) (#& . 85) (#& . 87) (#& . 92) (#& . 83) (#& . 44) (#& . 48) (#& . 42) (#& . 45) (#& . 46) (#& . 49) (#& . 52) (#& . 50) (#& . 53) (#& . 54) (#& . 55) (#& . 82) (#& . 81) (#& . 79) (#& . 75) (#& . 72) (#& . 60) (#& . 56) (#& . 98) (#& . 71) (#& . 66) (#& . 70) (#& . 64) (#& . 69) (#& . 67))) ((((∀ ALIST)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST)))) ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST))))))) . (AXIOM (TM& ((∀ ALIST)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST)))) ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . ALIST)))))))) . ((CAR #& . 29) (ATOM #& . 1) (NULL #& . 26) (ALISTP #& . 57) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 53 .) (GROUND . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 95) . VARIABLE .) (GROUND . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 95) . VARIABLE .) (NIL . (DECL (A B C) (TYPE: (TY& . GROUND))) . ((C #& . 94) (B #& . 96) (A #& . 97)) . NIL . NIL . NIL . LISPAX . NIL . 11 .) (GROUND . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 95) . VARIABLE .) ((((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (META& NIL)) (((∀ X U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) (((∀ U)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (META& NIL)) (((∀ X U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) (((∀ U)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . U)))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 76) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 30 .) ((((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL (((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)))) (((∀ X Y)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . Y))) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))))) (((∀ X)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X))))) . (AXIOM (TM& ((∀ PHI)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL (((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)))) (((∀ X Y)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . Y))) ((SYMBOL& NIL . PHI) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))))) (((∀ X)) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)))))) . ((ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 76) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 33 .) ((→ (⊗ GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 83) . VARIABLE .) ((→ (⊗ GROUND GROUND GROUND GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 83) . VARIABLE .) ((→ (* GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 87) . VARIABLE .) ((→ (⊗ GROUND GROUND GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 87) . VARIABLE .) ((((∀ NILCASE DEF)) NIL (((∃ FUN)) NIL (((∀ PARS X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (META& NIL) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . NILCASE) NIL (SYMBOL& NIL . PARS))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEF) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS))))))) . (AXIOM (TM& ((∀ NILCASE DEF)) NIL (((∃ FUN)) NIL (((∀ PARS X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (META& NIL) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . NILCASE) NIL (SYMBOL& NIL . PARS))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEF) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS)))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (PARS #& . 84) (FUN #& . 86) (DEF #& . 88) (NILCASE #& . 89)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 32 .) ((→ (⊗ GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 87) . VARIABLE .) (NIL . (DECL PARS (TYPE: (TY& * GROUND))) . ((PARS #& . 84)) . NIL . NIL . NIL . LISPAX . NIL . 31 .) ((* GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 85) . VARIABLE .) ((((∀ ATOMCASE DEFSEXP)) NIL (((∃ FUN)) NIL (((∀ PARS X Y)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . ATOMCASE) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEFSEXP) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS))))))) . (AXIOM (TM& ((∀ ATOMCASE DEFSEXP)) NIL (((∃ FUN)) NIL (((∀ PARS X Y)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . ATOMCASE) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . FUN) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . DEFSEXP) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . PARS)) ((SYMBOL& NIL . FUN) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . PARS)) (SYMBOL& NIL . PARS)))))))) . ((ATOM #& . 1) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (PARS #& . 84) (FUN #& . 86) (DEF #& . 88) (NILCASE #& . 89) (DEFSEXP #& . 90) (ATOMCASE #& . 91)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 34 .) ((((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . V) (SYMBOL& NIL . W))))) . (AXIOM (TM& ((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . V) (SYMBOL& NIL . W)))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 46 .) ((((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)) (SYMBOL& NIL . W)))) . (AXIOM (TM& ((∀ U V W)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V) (SYMBOL& NIL . W)) ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)) (SYMBOL& NIL . W))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 47 .) ((→ (⊗ (→ GROUND TRUTHVAL) GROUND) TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 79) . VARIABLE .) ((((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (META& NIL)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))))) . (AXIOM (TM& ((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (META& NIL)) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ALLP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 76) (CONS #& . 21) (ALLP #& . 80)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 48 .) ((→ (⊗ (→ GROUND TRUTHVAL) GROUND) TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 75) . VARIABLE .) (NIL . (DECL (PHI) (TYPE: (TY& → GROUND TRUTHVAL))) . ((PHI #& . 76)) . NIL . NIL . NIL . LISPAX . NIL . 12 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 77) . VARIABLE .) ((((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (META& NIL))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U)))))) . (AXIOM (TM& ((∀ PHI X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (META& NIL))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . PHI) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . SOMEP) NIL (SYMBOL& NIL . PHI) (SYMBOL& NIL . U))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (PHI #& . 76) (CONS #& . 21) (SOMEP #& . 78)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 49 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 72) . VARIABLE .) ((→ (⊗ (→ GROUND GROUND) GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 72) . VARIABLE .) ((((∀ FN X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . FN) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (SYMBOL& NIL . U)))))) . (AXIOM (TM& ((∀ FN X U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . FN) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . MAPCAR) NIL (SYMBOL& NIL . FN) (SYMBOL& NIL . U))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (MAPCAR #& . 73) (FN #& . 74)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 50 .) ((((∀ XA Y ALIST)) NIL ((SYMBOL& NIL . ALISTP) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST)))) . (AXIOM (TM& ((∀ XA Y ALIST)) NIL ((SYMBOL& NIL . ALISTP) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST))))) . ((ATOM #& . 1) (ALISTP #& . 57) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (ZA #& . 5) (YA #& . 7) (XA #& . 8) (CONS #& . 21) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 54 .) ((((∀ X XA Y ALIST)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . XA)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST)))))) . (AXIOM (TM& ((∀ X XA Y ALIST)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (META& NIL)) (META& NIL)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) (SYMBOL& NIL . ALIST))) ((SYMBOL& NIL . CONDI) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . XA)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . XA) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST))))))) . ((ATOM #& . 1) (ALISTP #& . 57) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (ZA #& . 5) (YA #& . 7) (XA #& . 8) (CONS #& . 21) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63) (ASSOC #& . 65)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 56 .) (NIL . (DECL MEMBER (TYPE: (TY& → (⊗ GROUND GROUND) TRUTHVAL)) (SYNTYPE: CONSTANT)) . ((MEMBER #& . 68)) . NIL . NIL . NIL . LISPAX . NIL . 58 .) ((→ (⊗ GROUND GROUND) TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 69) . CONSTANT .) ((((∀ X Y U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (META& NIL))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ∨) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) . (AXIOM (TM& ((∀ X Y U)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (META& NIL))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . Y) (SYMBOL& NIL . U))) ((SYMBOL& NIL . ∨) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)) ((SYMBOL& NIL . MEMBER) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (MEMBER #& . 68)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 59 .) (NIL . (DECL ASSOC (TYPE: (TY& → (⊗ GROUND GROUND) GROUND)) (SYNTYPE: CONSTANT)) . ((ASSOC #& . 65)) . NIL . NIL . NIL . LISPAX . NIL . 55 .) ((→ (⊗ GROUND GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 66) . CONSTANT .) ((((∀ X ALIST)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST)))) . (AXIOM (TM& ((∀ X ALIST)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . ASSOC) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . ALIST))))) . ((ALISTP #& . 57) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63) (ASSOC #& . 65)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 57 .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (NIL . (DECL (ALIST A0 A1 A2) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . ALISTP))) . ((A2 #& . 59) (ALISTP #& . 57) (A1 #& . 61) (ALISTP #& . 57) (A0 #& . 62) (ALISTP #& . 57) (ALIST #& . 63) (ALISTP #& . 57)) . NIL . NIL . NIL . LISPAX . NIL . 51 .) (GROUND . (SYMBOL& NIL . ALISTP) . NIL . NIL . (#& . 60) . VARIABLE .) (NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP #& . 57)) . NIL . NIL . NIL . LISPAX . NIL . 6 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . (#& . 58) . CONSTANT .) ((((∀ ALIST)) NIL ((SYMBOL& NIL . LISTP) NIL (SYMBOL& NIL . ALIST))) . (AXIOM (TM& ((∀ ALIST)) NIL ((SYMBOL& NIL . LISTP) NIL (SYMBOL& NIL . ALIST)))) . ((LISTP #& . 10) (ALISTP #& . 57) (A2 #& . 59) (A1 #& . 61) (A0 #& . 62) (ALIST #& . 63)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 52 .) ((((∀ X V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . V)))) . (AXIOM (TM& ((∀ X V)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . V))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 45 .) ((((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (META& NIL)) (SYMBOL& NIL . U))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (META& NIL)) (SYMBOL& NIL . U)))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 44 .) ((((∀ X U V)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (META& NIL) (SYMBOL& NIL . V)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)))))) . (AXIOM (TM& ((∀ X U V)) NIL ((SYMBOL& NIL . ∧) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL (META& NIL) (SYMBOL& NIL . V)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . APPEND) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)) (SYMBOL& NIL . V)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V))))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 43 .) (NIL . (DECL APPEND (TYPE: (TY& → (⊗ GROUND (* GROUND)) GROUND)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840)) . ((APPEND #& . 51)) . NIL . NIL . NIL . LISPAX . NIL . 41 .) ((→ (⊗ GROUND (* GROUND)) GROUND) . (SYMBOL& NIL . UNIVERSAL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . (#& . 52) . CONSTANT .) ((((∀ U V)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V)))) . (AXIOM (TM& ((∀ U V)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . APPEND) NIL (SYMBOL& NIL . U) (SYMBOL& NIL . V))))) . ((LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (APPEND #& . 51)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 42 .) ((((∀ X LST)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . LST)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST))))) . (AXIOM (TM& ((∀ X LST)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . LST)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST)))))) . ((SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (LIST #& . 43) (LST #& . 47)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 40 .) (NIL . (DECL LST (TYPE: (TY& * GROUND))) . ((LST #& . 47)) . NIL . NIL . NIL . LISPAX . NIL . 36 .) ((* GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 48) . VARIABLE .) ((((∀ LST)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST)))) . (AXIOM (TM& ((∀ LST)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . LST))))) . ((LISTP #& . 10) (LIST #& . 43) (LST #& . 47)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 39 .) ((((∀ X)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL)))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (META& NIL))))) . ((SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21) (LIST #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 38 .) (NIL . (DECL LIST (TYPE: (TY& → (* GROUND) GROUND)) (SYNTYPE: CONSTANT)) . ((LIST #& . 43)) . NIL . NIL . NIL . LISPAX . NIL . 35 .) ((→ (* GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . NIL . (#& . 44) . CONSTANT .) ((((∀ X)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X)))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . LIST) NIL (SYMBOL& NIL . X))))) . ((LISTP #& . 10) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (LIST #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 37 .) ((((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X))) (SYMBOL& NIL . X)))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X))) (SYMBOL& NIL . X))))) . ((CAR #& . 29) (CDR #& . 24) (ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 29 .) ((((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U))) (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CONS) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)) ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U))) (SYMBOL& NIL . U))))) . ((CAR #& . 29) (CDR #& . 24) (NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 28 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CDR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . Y))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CDR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . Y)))) . ((CDR #& . 24) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 27 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . X))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . =) NIL ((SYMBOL& NIL . CAR) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))) (SYMBOL& NIL . X)))) . ((CAR #& . 29) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 26 .) ((((∀ X U)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ X U)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))))) . ((NULL #& . 26) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 25 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))))) . ((ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 24 .) ((((∀ X Y)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y)))) . (AXIOM (TM& ((∀ X Y)) NIL ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . Y))))) . ((SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 23 .) ((((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (META& NIL) (SYMBOL& NIL . U)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (META& NIL) (SYMBOL& NIL . U)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))))) . ((NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 22 .) ((((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . U) (META& NIL)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ≡) NIL ((SYMBOL& NIL . =) NIL (SYMBOL& NIL . U) (META& NIL)) ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))))) . ((NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 21 .) ((((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X))))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . X)))))) . ((CDR #& . 24) (ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 20 .) ((((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X))))) . (AXIOM (TM& ((∀ X)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . ATOM) NIL (SYMBOL& NIL . X))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . X)))))) . ((CAR #& . 29) (ATOM #& . 1) (SEXP #& . 3) (Z #& . 17) (Y #& . 19) (X #& . 20)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 19 .) (NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR #& . 29)) . NIL . NIL . NIL . LISPAX . NIL . 1 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . (#& . 30) . CONSTANT .) ((((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . SEXP) NIL ((SYMBOL& NIL . CAR) NIL (SYMBOL& NIL . U)))))) . ((CAR #& . 29) (NULL #& . 26) (LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 18 .) (NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL #& . 26)) . NIL . NIL . NIL . LISPAX . NIL . 4 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . (#& . 27) . CONSTANT .) (NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& → GROUND GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR #& . 24)) . NIL . NIL . NIL . LISPAX . NIL . 2 .) ((→ GROUND GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . (#& . 25) . CONSTANT .) ((((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U))))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . ⊃) NIL ((SYMBOL& NIL . ¬) NIL ((SYMBOL& NIL . NULL) NIL (SYMBOL& NIL . U))) ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CDR) NIL (SYMBOL& NIL . U)))))) . ((CDR #& . 24) (NULL #& . 26) (LISTP #& . 10) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 17 .) (NIL . (DECL CONS (TYPE: (TY& → (⊗ GROUND GROUND) GROUND)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS #& . 21)) . NIL . NIL . NIL . LISPAX . NIL . 13 .) ((→ (⊗ GROUND GROUND) GROUND) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . (#& . 22) . CONSTANT .) (GROUND . (SYMBOL& NIL . SEXP) . NIL . NIL . (#& . 18) . VARIABLE .) (GROUND . (SYMBOL& NIL . SEXP) . NIL . NIL . (#& . 18) . VARIABLE .) (NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . SEXP))) . ((Z #& . 17) (SEXP #& . 3) (Y #& . 19) (SEXP #& . 3) (X #& . 20) (SEXP #& . 3)) . NIL . NIL . NIL . LISPAX . NIL . 9 .) (GROUND . (SYMBOL& NIL . SEXP) . NIL . NIL . (#& . 18) . VARIABLE .) ((((∀ X U)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U)))) . (AXIOM (TM& ((∀ X U)) NIL ((SYMBOL& NIL . LISTP) NIL ((SYMBOL& NIL . CONS) NIL (SYMBOL& NIL . X) (SYMBOL& NIL . U))))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15) (Z #& . 17) (Y #& . 19) (X #& . 20) (CONS #& . 21)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 16 .) (GROUND . (SYMBOL& NIL . LISTP) . NIL . NIL . (#& . 13) . VARIABLE .) (GROUND . (SYMBOL& NIL . LISTP) . NIL . NIL . (#& . 13) . VARIABLE .) (NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . LISTP))) . ((W #& . 12) (LISTP #& . 10) (V #& . 14) (LISTP #& . 10) (U #& . 15) (LISTP #& . 10)) . NIL . NIL . NIL . LISPAX . NIL . 8 .) (GROUND . (SYMBOL& NIL . LISTP) . NIL . NIL . (#& . 13) . VARIABLE .) (NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP #& . 10)) . NIL . NIL . NIL . LISPAX . NIL . 5 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . (#& . 11) . CONSTANT .) ((((∀ U)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . U))) . (AXIOM (TM& ((∀ U)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . U)))) . ((LISTP #& . 10) (SEXP #& . 3) (W #& . 12) (V #& . 14) (U #& . 15)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 15 .) (GROUND . (SYMBOL& NIL . ATOM) . NIL . NIL . (#& . 6) . VARIABLE .) (GROUND . (SYMBOL& NIL . ATOM) . NIL . NIL . (#& . 6) . VARIABLE .) (NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& SYMBOL& NIL . ATOM))) . ((ZA #& . 5) (ATOM #& . 1) (YA #& . 7) (ATOM #& . 1) (XA #& . 8) (ATOM #& . 1)) . NIL . NIL . NIL . LISPAX . NIL . 10 .) (GROUND . (SYMBOL& NIL . ATOM) . NIL . NIL . (#& . 6) . VARIABLE .) (NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP #& . 3)) . NIL . NIL . NIL . LISPAX . NIL . 7 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . (#& . 4) . CONSTANT .) (NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& → GROUND TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM #& . 1)) . NIL . NIL . NIL . LISPAX . NIL . 3 .) ((→ GROUND TRUTHVAL) . (SYMBOL& NIL . UNIVERSAL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . (#& . 2) . CONSTANT .) ((((∀ XA)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . XA))) . (AXIOM (TM& ((∀ XA)) NIL ((SYMBOL& NIL . SEXP) NIL (SYMBOL& NIL . XA)))) . ((ATOM #& . 1) (SEXP #& . 3) (ZA #& . 5) (YA #& . 7) (XA #& . 8)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . 14 .))